k:, f:(int_seg(0; k)).
increasing(f; k)  guard((x,y:int_seg(0; k). (x < y)  ((f(x)) < (f(y))))) 

latex

Definitions	prop{i:l}, t  T, guard(T), P  Q, x:A. B(x), False, A, A  B, ge(i; j), P  Q, lelt(i; j; k), int_seg(i; j), increasing(f; k),
Lemmas	nat wf, increasing wf, int seg wf, ge wf, nat properties, le wf